perm filename W77.OUT[LET,JMC] blob
sn#274158 filedate 1977-04-05 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 ∂14-Mar-77 1353 JMC
C00034 ENDMK
C⊗;
∂14-Mar-77 1353 JMC
To: RWW
I think the FOL jproject should be described in a way that shows
change. Why don't you try to put it into the following format.
The FOL proof-checker is now able to check almost all
the kinds of reasoning for which it was designed.
Weyhrauch (1977) is a collection of these proofs. As expected, they
are longer than human informal proofs, but they are about the
first machine-checked complete proofs of substantial results
in mathematics, program correctness, and the theory of knowledge.
We are now
entering a new phase of the work. The next step is to reduce
the size of the human contribution to the reasoning by introducing
shortcuts. A large group of shorcuts has been programmed and
are ready to be tested on substantial problems. These included
a.
b.
During the next year and a half, we plan the following
proofs:
∂14-Mar-77 1338 JMC
To: ZM
Please look at mtc.pro[w77,jmc]. No protection.
∂14-Mar-77 1222 JMC
To: carl at MIT-AI
You may be interested in EXOTIC[W77,JMC]. I would welcome your comments.
∂14-Mar-77 1154 JMC
To: MJL
Tomorrow at 4:00 is ok. Please confirm.
∂14-Mar-77 0944 JMC
To: JAB
Your suggestion seems fine. Yes, you may audit.
∂13-Mar-77 1745 JMC Your writeup.
To: CG
Yours is too technical for ARPA. It would need a Scientific American
level summary. Also it is somewhat remote from application - even
for me. However, it isn't essential that you have one. Naturally,
I would hope you would do something more on non-knowledge also.
∂12-Mar-77 2354 JMC
To: ME
;:;oooogggggggggggggggooooooooooggggggggggggg99ll
∂12-Mar-77 1525 JMC
To: *
Can anyone give a reference to a mathematical treatment of Instant Insanity? - JMC
∂12-Mar-77 1506 JMC Colloquium
To: MJL
Please tell whoever is in charge of the colloquium
(Is it still Frances Yao?) that I would like to
give one entitled "Representing Recursive Programs in First
Order Logic".
∂12-Mar-77 1056 JMC
To: rsmith at RUTGERS-10
Just checking if mail to rutg works.
∂12-Mar-77 1055 JMC
To: smith at RUTGERS-10
Just checking if mail to rutg works.
∂12-Mar-77 1055 JMC
To: rs at RUTGERS-10
Just checking if mail to rutg works.
∂12-Mar-77 1050 JMC
To: joseph at MIT-MC
I haven't drawn a precise line in my mind, and it isn't necessary to
have a precise line in order to decide some cases. Certainly I would
say that anyone not charged with a crime is entitled to leave any
country including his own. This is what the U.N. Declaration on human
rights says. If there were an absolute right to depart, one country
might give sanctuary to another's criminals as a means of encouraging
crime in that country, but I doubt many would find it worthwhile.
Castro found the hijackers a pain in the neck, and I wonder it the
North Koreans, who, I seem to remember, offered to take the Attica
rebel prisoners, would have been happy with them. An absolute agreement
to let anyone out wouldn't be bad. We wouldn't even lose too much
if we unilaterally let all spies go except those, if any, who had
just stolen a vital secret (if any) and hadn't been able to transmit
it.
∂12-Mar-77 0204 JMC
To: MJC
I was here first
∂10-Mar-77 1636 JMC Conjecture fails.
To: MFB, ND
tau[f](x) = if f h1 x = omega ∧ f h2 x = omega then omega else 1
is continuous but not of the usual form, i.e. it can't be written
without explicit mention of omega, and it can't be computed except
by computing f h1 x and f h2 x in parallel so that whichever returns
causes tau[f](x) to have value 1.
∂10-Mar-77 1624 JMC Not really a new case.
To: MFB
We have not mentioned, but have always had the case
tau[f](x) = m1(x,f h x).
Its least fixed point is the totally undefined function. But
if m f h x then g1 x else g2 x = m1(x,f h x)
where
m1(x,y) = if m y then g1 x else g2 x.
∂10-Mar-77 1054 JMC
To: feigenbaum at SUMEX-AIM
I hope the title of "Professor of Combinatorics" for Chvatal remains,
because this was an essential factor in my positive vote in allowing
me to hope that the appointment wouldn't unduly mortgage the chances
of getting new people in C.S., especially AI.
∂10-Mar-77 1050 JMC
To: bobrow at PARC-MAXC
I am glad to accept your invitation, and the deadline offers no problem.
∂09-Mar-77 1759 JMC
To: PAT
Please fill out the form on Gumb's proposal using nsf.re2[let,jmc].
∂09-Mar-77 1603 JMC
To: MJL
How much does one have to drink for the AA Qual?
∂08-Mar-77 2207 JMC
To: ME, LES
I am not much impressed with the cost-effectiveness of the latest E mods.
∂08-Mar-77 1549 JMC Guy Steele visit
To: gls at MIT-AI
CC: RWG, LES
We will be glad to have you in July in accordance with the suggestions
in your message to Knuth and Gosper, and we can help with expenses.
∂07-Mar-77 1423 JMC
To: dbrown at SUMEX-AIM, feigenbaum at SUMEX-AIM
Oral announcement.
∂07-Mar-77 1151 JMC
To: feigenbaum at SUMEX-AIM, dbrown at SUMEX-AIM
AI Lab policy on CSD use
1. We hereby offer accounts to all CSD faculty. Message use and
document preparation are solicited. If use by typists is wanted, this
can be negotiated. Arrange accounts with Lester Earnest at the Lab.
The Lab can't provide terminals, but we recommend Datamedias in the
configuration that our editor supports.
Faculty members should state whether they plan to log in
often enough so that messages are reliably received.
2. PhD students who request accounts will receive them with
probability near one. Preparation of theses is tentatively welcome.
We reserve the right to get stingy if we are overwhelmed, but we don't
expect it.
3. Use properly belonging on other machines is not welcomed.
Thus students with RAs on projects using SUMEX or IMSSS are expected to use
those computers, and students taking courses that use LOTS are expected
to do the course work on LOTS.
4. No-one should log in on the AI Lab computer remotely and
then go out on the ARPA net or dial-out lines. These programs
use up memory space and computer time out of proportion to what they
accomplish. Remote computers should be used directly.
5. We don't want to post this policy. Stanford owns the KL-10
received as a gift from D.E.C. and other equipment given us by the
government. The government owns some of the equipment and pays for
maintenance. Figuring out the exact fraction of the computer we can
thereby dispose of for non-government purposes would be complicated
and subjective and is better put off until it becomes necessary for
other reasons.
∂07-Mar-77 0110 JMC
To: LES
If you agree, I'll send POLICY[W77,JMC] to Feigenbaum and D. Brown.
∂06-Mar-77 1351 JMC
CC: dbrown at SUMEX-AIM
les,feigenbaum%sumex
∂06-Mar-77 1342 JMC Your request.
To: TOG
I have inquired, and no-one has a project for which they
consider you suitable. Furthermore, you ran up a big Pony
bill and haven't paid it. Please don't use this computer
any more.
∂05-Mar-77 1212 JMC
To: pratt at MIT-AI
No, I haven't been thinking about CGOL though I may get back to it.
∂05-Mar-77 1211 JMC
CC: JBR, LES, PMF
∂05-Mar-77 0232 TOG ACCOUNTS
JOHN, IS THERE A PROJECT THAT COULD USE SOME HELP,I WOULD LIKE TO USE THE
FACILITY? TODD GLASSEY
∂02-Mar-77 2335 JMC
To: DEK
Thanks for the loan of the tiles.
∂02-Mar-77 2215 JMC
To: MFB
Since you may have to refer to it, remember it's spelled Vuillemin.
∂02-Mar-77 1616 JMC MI9
To: phw at MIT-AI, buchanan at SUMEX-AIM
The attendance, including the Soviet attendance, at MI9 looks interesting
enough so that I have decided to go.
∂02-Mar-77 1143 JMC
To: HVA
I don't remember any such thing, but you'd better check such matters
directly. I try to turn over such communications to you or Les.
∂02-Mar-77 1057 JMC
To: AIQUAL.LST[W77,JMC]:;
I have asked Moira to post a notice asking who intends to take the
qual. We can then decide on format.
∂01-Mar-77 2247 JMC Movie Projector
To: LES
If, as seems likely, our projector has been stolen again, I
suggest the next one be chained and bolted to a wheeled table.
∂01-Mar-77 1803 JMC
To: TED
The terminal in Martin Davis's office squeals like a dying bat.
∂28-Feb-77 2108 JMC
To: ALS, ME
The page on Imlacs in the E manual is outdated and should be deleted.
∂27-Feb-77 2216 JMC
To: minsky at MIT-AI
Thanks, I'll transmit content to Suppes.
∂27-Feb-77 2100 JMC
To: JAB
Yes, it would.
∂25-Feb-77 1851 JMC
To: PAT
DIALNE.LST contains some notes on who should get Dialnet memos.
Please ask me for help in making it into a proper list.
∂25-Feb-77 0958 JMC
To: JAB
It would be important for both LOTS and SRI to maintain compatibility
with M.I.T.
∂23-Feb-77 2346 JMC
To: DSB
There is no prospect of replacing the ADM3s for two years.
∂23-Feb-77 1320 JMC
CC: PMF, RPG
∂23-Feb-77 1312 FTP:Dang at SRI-AI Maclisp for Tops-20
Date: 22 Feb 1977 2318-PST
From: Dang at SRI-AI
Subject: Maclisp for Tops-20
To: JCM at SAIL
cc: JAB at SAIL, DanG
Hello. John Borchek was telling me that you wanted to have a copy of
Maclisp on Lots, possibly to be used in a lisp course at Stanford.
Right now I am in the middle of trying to make Maclisp run a little
better under Tops-20, but I can give you the origional Tops-10 version
of Maclisp 1251 running with the DEC PA1050 compatibility package.
So far it appears to be working just fine, but since nobody is supporting
Maclisp for Tops-20 except for the limited amount of work that I have
been doing, I would really appreciate it if you could forward all comments,
bugs, and fixes to me and I will look into fixing it for our users here
at SRI too. I will also add your name, as well as anyone else you like,
to the Maclisp distribution list that I am preparing so that you will
get the information on newer versions of Maclisp as they are created.
On the tape that I am will drop by tomorrow, I am adding the compiler
(Ncomplr), Grindef, Pratt's CGOL, as well as other assorted library
routines that might be useful. I will send over another tape at a
later date containing more library routines from MIT-MC as I tranport
them. Most of this has not been tested much either, if at all, so
again, use them with care.
If there is any way at all that I can assist you, please feel free
to send me a message.
Dan Gerson
-------
∂23-Feb-77 0930 JMC via USCT
To: LES
Received somewhat soothing message from Russell.
∂23-Feb-77 0925 JMC via USCT
To: russell at USC-ISI
Sorry mixed my message to you with Ed's message to me.
∂23-Feb-77 0907 JMC
To: russell at USC-ISI
∂23-Feb-77 0313 FTP:Feigenbaum at SUMEX-AIM march 4 meeting at arpa
Date: 22 FEB 1977 1817-PST
From: Feigenbaum at SUMEX-AIM
Subject: march 4 meeting at arpa
To: les at SU-AI, jmc at SU-AI
The meeting on March 4 is in the MORNING, not afternoon as
previously mentioned. Participants from Stanford are jmc,les,and eaf.
Particiaants on their side are col. russell and I don't know who else.
ed
-------
I understsand your position better now. We have nsf visit
Thurs and Fri at which I can raise question of thix their
support of basic AI work aaxx at Stanford. I will try
to phone you on Monday.
∂22-Feb-77 0207 JMC
To: PAT
Please xs sato.xgp[w77,jmc] and sato.xgp[let,jmc]. I'll be back Thurs.
∂21-Feb-77 0110 JMC
To: ZM
What is the reference on subgoal induction?
∂20-Feb-77 2205 JMC
To: PMF
I have put part3.xgp in [206,lsp] which is where it should be.
∂20-Feb-77 1629 JMC
To: WHG
I take it back. I now think call-by-value is right.
∂19-Feb-77 1407 JMC
To: RSC
FIRST and FIRST.NEW on [W77,JMC] may interest. They are evolving.
∂19-Feb-77 1000 JMC Dirt and mess
To: LES, HVA
How can we get the machine room and other places cleaned up?
I suspect they make a bad impression on funders.
∂18-Feb-77 1337 JMC Theoretical work in AI
To: russell at USC-ISI
Is it correct than ARPA is no longer willing to support
theoretical work in AI? There is already too little theoretical
work as it is, and I would like the opportunity to argue this
point.
∂18-Feb-77 1119 JMC
To: JBR
How is a load average of .8 compatible with a disk queue of 18?
∂18-Feb-77 1000 JMC dialer
To: TED
The dialer isn't working again. When it dials a number, it lets it ring
once and then reports a time-out error. Perhaps the timer is just set
too short.
∂17-Feb-77 2044 JMC Machine Intelligence Workshop
To: phw at MIT-AI
Do you remember who else Michie said was going from this country. We could
tell Michie to tell the Russians that attendance would be great if
Lerner received an exit visa.
∂17-Feb-77 1624 JMC
To: *
5505 is reserved for a demo from 8:30 to 10:30 tonight Thursday
∂16-Feb-77 2150 JMC
To: DCL
It appeared in a book edited by Tom Steele with a title like
"Formal language definition languages". Maybe I can find it, and since
I don't recall it as a popular paper, there may still be reprints.
∂16-Feb-77 1459 JMC Non-autologut.
To: EJG
As long as I am so subject to interruption, I need to keep the privilege.
I have no objection to your suggestion, but elaboration of the privilege
structure is very low priority.
∂16-Feb-77 1458 JMC
To: RS
Many thanks for Ulam's book which I have just read.
∂14-Feb-77 2152 JMC
To: BPM
Well, if someone were to rewrite Telnet for greater efficiency, ...
∂14-Feb-77 2103 JMC IMSSS and TELNET
To: BPM, TOB
These programs are quite expensive to use. Communication with other
computers from remote terminals should be done directly or through the
TIP whenever possible. BPM was just taking 26% PL.
∂14-Feb-77 1407 JMC
To: RWW
It will have the extension .prf if it still exists.
∂12-Feb-77 1625 JMC
To: DCL
What are the other reasons?
∂11-Feb-77 2343 JMC
To: PMF
It would be good to get some Lisp on LOTS quite soon.
∂11-Feb-77 1810 JMC A Natural Representation
To: ND, WP
The result came out better than I expected. I have put notes in your
boxes, but you can also read REPRES[W77,JMC] if you don't mind the PUB.
∂11-Feb-77 1526 JMC Jarvis board
To: PMF
John Gill, ESL, is interested in getting one or two for the PDP-11
they are expecting in May. You might call him about the present
state of the redesign.
∂11-Feb-77 1503 JMC
To: *
USGS earthquake predictors can hire student to work on data handling.
Call Chuck Bufe, 323-8111 x2568
∂11-Feb-77 1011 JMC DIAL
To: JBR
Erik Gilbert was using DIAL last night at 10 chars/sec and achieved
a PL of 14%. If the KL does an instruction per microsecond, this
represents 14,000 instruction executions per character transferred.
How can this be?
∂11-Feb-77 0132 JMC
To: ND
If I understand your formula correctly, then the recursive definition
f x ← if p x then x else f h x
gives rise to the sentence
∀x.(y = f x ≡ ∃w.[x.y ε w ∧ ∀u v.[u.v ε w ⊃ ∀z.[(h u . z) ε w ∧
v = if p u then u else z]]]).
This doesn't seem right. It looks like ∀z should read ∃z, but
even then the terminating case isn't handled right. I think we
want
∀x.(y = f x ≡ ∃w.[x.y ε w ∧ ∀u v.[u.v ε w ⊃
if p u then v = u else ∃z.[(h u . z) ε w].
No, this doesn't work either, because the recursive definition
f x ← f x
would let us conclude that f x = 196.
∂10-Feb-77 2023 JMC
To: RPG
I have FTPed the file to PART3[W77,JMC], but it doesn't seem to be
lineprinter PUB output. What do you make of it?
∂10-Feb-77 1916 FTP:ELLEN at MIT-MC (V. Ellen Lewis )
Date: 10 FEB 1977 2217-EST
Sender: ELLEN at MIT-MC
From: ELLEN at MIT-MC (V. Ellen Lewis )
To: jmc at SU-AI
Message-ID: <[MIT-MC].34095>
Hello. I apologise for the delay. The draft of the LISP Manual which you
have is Parts 1 and 2, which are now available. Part 3, which considers the
LISP system in general, will (very strong future tense! -- I also work with
Bill Martin so am versed in semantics, syntax, etc! --) be at the printers
by the end of next week, or at worst by the end of February. A draft copy
of this part can be had if you FTP to SAIL MC:ELLEN;PART3 DOC (lineprinter
Pub output...).
Many thanks for part 3.
∂10-Feb-77 1936 JMC
To: ellen at MIT-MC
Many thanks for part 3.
∂10-Feb-77 1706 JMC
To: carl at MIT-AI
I accept with pleasure.
∂10-Feb-77 1037 JMC
To: DSB
I can give you a copy of a paper I gave at AAAS meeting last year.
There has been much enthusiasm for cable TV in this connection, but
I am not one of the enthusiasts, because (i) the telephone system
is good enough in performance and cost (ii) cable TV is not everywhere
yet, and the rest of the required technology is ready to go (iii)
cable TV is structured as a set of local monopolies whose main
business is in TV, so new services will be dominated by the interests
of the cable TV company.
∂09-Feb-77 1656 JMC
To: RWW
Vera and I accept with pleasure. It's 7pm, isn't it?
∂09-Feb-77 1137 JMC
To: phw at MIT-AI
I wrote to Meltzer that the paper should be published as revised.
∂09-Feb-77 0526 JMC Lisp equations
To: MDD
What can be said about solving Lisp equations, e.g.
((x . a) . y) = (y . (b . a)). They are in some respects
simpler than string equations because of the lack of
associativity, but they may be more important in relation
to pattern recognition.
∂08-Feb-77 0720 JMC
To: PAT
Have you looked for a letter asking about Wise in the incoming?
∂07-Feb-77 1921 JMC your proof
To: WP
It seems to me to be a metamathematical argument. Can you give an
argument that involves just substituting a suitable function for
g, as my converse argument involved just making q(x,y) ≡ y = g(x)?
∂07-Feb-77 1407 JMC 256K core
To: dbrown at SUMEX-AIM, feigenbaum at SUMEX-AIM
As you probably know the rest of our core was installed
last Thursday morning. It has made a big improvement. With 30
users, they were getting 22percent before and 62 percent after.
Incidentally, CMU still doesn't have 256K core, which accounts
for their bad experience. Theirs is overdue.
∂06-Feb-77 0021 JMC
To: pratt at MIT-AI
I'll study CGOL and make some suggestions, but it is unlikely that
a local dialect will arise here, because I have other things to do,
and the MACLISP hackers here, Dick Gabriel and Martin Brooks, don't
use CGOL. I guess I don't even know how the present Lisp compiler
treats iteration.
∂05-Feb-77 1917 JMC reply
To: pratt at MIT-AI
Got your message. Think we might be able to come close to agreement,
and I'll try to work out a desirable notation, but first I must try out
CGOL some more so as to avoid pointless innovation.
∂05-Feb-77 1832 JMC Bureaucracy
To: LES
It seems to me that if an unknown manages to use a large amount of
computer time, bureaucracy conceals who it was, because miscellaneous
is merely totalled. Any account using over a trivial amount should
be listed in bureaucracy.
∂05-Feb-77 1826 JMC Datapoint emulator in Telnet
To: JBR
I observed a random refugee from M.I.T. called ED on his way to
Antarctica using 20 percent of the computer in Telnet. It seems
he was using a Datapoint Emulation feature in Telnet that Gosper
says Stallman installed on a visit. Suggest you disable it.
∂05-Feb-77 1741 JMC
To: LES
I missed him, but ED seems to be an M.I.T. hacker far from home.
∂05-Feb-77 1545 JMC CGOL.GRU[W77,JMC]
To: pratt at MIT-AI
This file contains the present state of my CGOL grumbles. As you will
see, I am trying to optimize something different from what you
have been optimizing. You will also note that I haven't got very far
into CGOL.
∂15-Mar-77 1315 JMC
To: nilsson at SRI-KL
Postponing the seminar to the 28th is fine with me.
∂16-Mar-77 0000 JMC
To: feigenbaum at SUMEX-AIM
title: Epistemological Problems of AI. Paper: McCarthy and Hayes - Some
Philosophical Problems from the Standpoint of Artificial Intelligence -
MI4. (I may recommend a new paper if it's ready in time, but I won't know
by the first day.)
∂16-Mar-77 0003 JMC
To: RCM
Thanks. It's quite usable.
∂16-Mar-77 0223 JMC
To: DCL
Yes. I called it to the musicians' attention today and will press them
to reduce it.
∂16-Mar-77 1025 JMC
To: PAM
Fine, I'll look today.
∂16-Mar-77 1143 JMC
To: DCL
jed works for Terry and is not a musician so far as we know.
∂16-Mar-77 1236 JMC
To: PAM
I couldn't find the manual on your desk.
∂16-Mar-77 1623 JMC
To: PAT
Please decorate suppes.le1
∂16-Mar-77 2216 JMC
To: JC
There are 5 220 jobs logged in now.
∂16-Mar-77 2220 JMC
To: JC
The 5 are SEK, KIP, RT, JOS, and BGH.
∂16-Mar-77 2227 JMC usage
To: SEK, KIP, RT, JOS, BGH
According to our agreement with John Chowning, Music 220 students, with
one exception whose name I forget, are supposed to use the machine between
3am and 9am. Music 220 was the largest single user group during the first
half of March, the second being other music use. The two amount to 35%,
of total usage which includes system services,
and this is much more than music's share. Please use the machine at the
agreed hours.
∂17-Mar-77 1511 JMC
To: PAM
1. I suggest you write one page on how to run MACLISP at LOTS and include
it with the manual you give to Moira tomorrow. It can be supplemented with
a handout later when we know more. If 35 is the estimated residual enrollment,
have them make 45.
∂18-Mar-77 0010 JMC
To: erman at CMU-10B
I'll have a definite reaction before your deadline, but my preliminary
reaction is that the two structure don't have the same fringe and
my SAMEFRINGE says so. The fringes are (A B NIL NIL) and (A NIL B NIL).
The problem refers to S-expressions not lists as I understood it, but
I want to look at how the others understood the problem.
∂18-Mar-77 1436 JMC
To: RDR
There isn't much point in publicity until facilities are actually
available.
∂18-Mar-77 1453 JMC
To: RDR
Yes, I get SCIP bulletin, and I don't share your suspicions.
∂18-Mar-77 1510 JMC
To: PAT
Please print andrei.le8[let,jmc] and include copies of mental, concep,
first, and minima.
∂18-Mar-77 1701 JMC
To: MJL
I would like to teach cs206 in fall and cs226 (representation problem
in AI) in Spring (preferably) or in Winter ( if it fits better).
∂19-Mar-77 0245 JMC Cache hits.
To: JBR
The fraction of cache hits might be increased by preferring to schedule
another job running E if the job just run was E.
∂19-Mar-77 1355 JMC
To: JBR
Yes, upper segment cache hits were all I was hoping for.
∂19-Mar-77 2135 JMC
To: KRD
I just received a belated announcement of a conference on AI and
philosophy. The conference announcement
lists many papers. There is a rather poor
paper in one of the IJCAI by Aaron Sloman.
I presume you meant my paper with Hayes; my paper with Painter was
on correctness of compilers. The file mental.xgp[f76,jmc] is such
a paper. Various philosophers like Nuel Belnap are intersted.
∂20-Mar-77 1216 JMC
To: LES
I agree with all that, and I'll be in this evening.
∂20-Mar-77 1232 JMC
To: reddy at CMU-10B
I would like to accept your invitation to visit Carnegie,
and Monday May 2 would be most convenient, since I want to spend
a week in Europe after the Repino meeting and want to teach my
Tuesday May 3 class. Is this OK. I want to plan the Pittsburgh
trip to reduce the costs in time and money of the MI9 trip.
∂20-Mar-77 1234 JMC
To: PAT
Please put the right address on sandew.le1 and pub it.
∂20-Mar-77 1239 JMC
To: PAT
Please put the right address on sandew.le1 and pub it.
Note how the accent on Linkoping is done.
I haven't checked it, so see if it comes out right.
∂22-Mar-77 1101 JMC
To: LES
Please check the numbers in carlst.me1[let,jmc].
∂22-Mar-77 1123 JMC
To: carlstrom at USC-ISI
CC: LES
Dear Dave:
We think ARPA is making a serious mistake in cutting so severely
the basic AI research, formal reasoning and mathematical theory of
computation parts of the proposal. Basic research is the foundation on
which applied research is based. We hope that our new proposal, which you
haven't seen yet, makes the connection between basic research and defense
applications better than we have in the past. We tried to present the
basic research in a way that will make it easy for you to expain its
relevance to management. Please let me know whether the new version is
helpful. Nevertheless, we despair that ARPA, having already decided to
reduce the effort, will be fully convinced.
There is, however, hope of getting other support, especially from
NSF for this work, although it will take some time, and it is difficult to
get money for research associates from NSF. Do you think the following
would be acceptable to ARPA?
1. We will proceed at the level of effort planned in our original
proposal.
2. We will charge ARPA for only a fraction of the project's costs.
3. The ARPA share would be 220K for basic AI and formal reasoning
and 80K for mathematical theory of computation totalling 300K compared to
566K in our original budget and 200K in your revised budget.
4. If other support is long delayed, we will sharply reduce the
level of effort, but we should have some word from NSF by Fall.
If ARPA cannot provide the additional 100K (to bring its share to
300K), then we will have to reduce the level of effort in July.
John McCarthy
∂22-Mar-77 1316 JMC
To: JC
CC: JAM
$70K plus tax and license?
∂23-Mar-77 1150 JMC
To: nilsson at SRI-KL
If I get NSF travel money.
∂24-Mar-77 0025 JMC
To: RWW
Martin Davis will be here today (Thursday).
∂24-Mar-77 0105 JMC Correctness of samefringe.
To: RWW
It looks like the following predicate will work for proving the termination
of samefringe: P(u) ≡ ∀x.(fringe x = u ⊃ ∀y.isetv samefringe(x,y)). The
proof is by ordinary structural induction on u. If you think it will work,
you might try to push it through.
∂24-Mar-77 0220 JMC
To: RWW
Equivalently P(u) ≡ ∀x y.(fringe x = u ⊃ isetv samefringe(x,y)).
∂25-Mar-77 2106 JMC
To: PAM
∂25-Mar-77 1644 PAM class notes
The entire department is shocked; your first 45 pages (and coincidently
45 copies) of class notes are ready. I have been told that the department
will pay for 50 pages of handouts per student, so I need to tell them
how much to charge for the class notes based on how many total
pages you will be handing out. I'll bring you back the original over the weekend.
Paul
Let's call it 110.
∂26-Mar-77 1138 JMC
To: gillogly at CMU-10A
Thanks, I have enough references.
∂26-Mar-77 2300 JMC
To: TW
WINOGRAD.FS[W77,JMC] is a draft of my Future Study comments on your paper.
∂27-Mar-77 1359 JMC
To: minsky at MIT-AI
Dear Marvin:
MINSKY.FS[F76,JMC] is a draft of my comments on your paper for the
Future Study. Besides that, there are a few rough edges that I suppose
you will want to iron out, so I haven't mentioned them in my direct
comments:
1. First it seems to me that you forgot the promise in the first
sentence to discuss "the problems and promises that arise from the
prospect of" AI. Recounting the opinions of science fiction writers seems
inadequate. You should either discuss it more or change the focus of the
introduction.
2. Ran out of time. There is no "second".
Best Regards,
∂27-Mar-77 2043 JMC
To: Dertouzos at MIT-MULTICS
I have finished all comments. You'll get them this week.
∂28-Mar-77 1246 JMC
To: minsky at MIT-AI
It is now page 18 of STUDY.FS[W77,JMC]. Sorry.
∂29-Mar-77 1549 JMC
To: PAM
Remind me to tell students charged $2.00 for notes to get $.80 refund.
∂31-Mar-77 1443 JMC
To: PHON[ESS,JMC]
Wegbreit 494-4432
∂31-Mar-77 2218 JMC
To: PAM, JAB
Please react to Gerson for LOTS.
∂01-Apr-77 1103 JMC
To: ryland at RUTGERS-10
1. We are operating with almost no security - either physical or
file - and plan to continue that way unless something bad happens.
The computer is available 24 hours a day without operators at any
time. At present there is a student guard at the building entrance,
but as soon as partitions have been installed to separate the
computer area from the education area which has no doors on the offices,
we expect to dspense with the guard.
We use the file security provided by TOPS-20. Each user has
a password, and he can protect his files or leave them public at his
choice. We have an accounting system, slightly modified from DEC's,
but since our users - restricted to students and unsponsored research -
are not ccarged, we use it only for monitoring purposes.
The languages in use include machine language, Fortran (DEC's)
SAIL (an Algol dialect), BLISS (from CMU; it's very expensive in computer
time), LISP (M.I.T.'s Maclisp), BASIC, MIX, PPL, and others.
∂01-Apr-77 2145 JMC
To: PAT
Find except that the return should be open from Stockholm. I'm staying in
Sweden for a few days.
∂02-Apr-77 1515 JMC
To: PAM
Please phone 321-7580 or 497-4430.
∂04-Apr-77 1030 JMC
To: MJL
How many now for the AI quals?
∂04-Apr-77 1102 JMC
To: berliner at CMU-10B
⊗berlin.me1
∂04-Apr-77 1121 JMC
To: ryland at RUTGERS-10
We will be interested in your experience. Details about ours can be obtained
from the Manager, Ralph Gorin, who is REG on this machine.
You may be interested in DIALNE[W77,JMC] which gives a plan for ARPANET like
communication using the ordinary telephone system. If you are interested in
participating in Dialnet, please let me know.
∂04-Apr-77 1211 JMC terminal
To: JMC
Thanks very much for the loan of the TI. It is a wonderful
gadget. I must conive to afford one.
Whit
p.s. It is on your desk.
∂04-Apr-77 1634 JMC MTC QUAL
To: dbrown at SUMEX-AIM
Martin Brooks tells me that he has the word that he must take an
MTC qual and that others are also interested. I am willing, with
the help of Zohar Manna which I shall solicit, to be in charge of one
given in late May. If this is in accordance with your and Ed's views,
send me a message and ask Moira to announce it and ask for signups.
It will be oral.
∂05-Apr-77 1021 JMC
To: berliner at CMU-10B
Do you think it would be possible to break with the tradition
of analyzing computer chess games as though they were human, i.e. where
you can't look into their heads? Could you persuade Slate and Atkins
to provide reasonably complete traces of what the machine was thinking
about at the critical points of the game with Levy and combine your
traditional chess player's analysis with your computer scientist's analysis
of where the machine misused its computational resources?
It would be good if Slate and Atkins could be persuaded to rerun
critical decisions, conceivably even with other parameters. Publishing
such an analysis in the SIGART Newsletter would
increase interest in better chess programs.
This is the message I tried to send yesterday.
∂05-Apr-77 2319 JMC
To: RWG
They are brothers.